nLab Feit-Thompson theorem

Contents

Contents

Statement

Theorem

Every finite group of odd order is a solvable group.

This is due to Feit & Thompson 1962.

A fully formalized proof in Coq has been produced by Gonthier et al. 2013.

References

The original proof:

  • Walter Feit, John Thompson: A solvability criterion for finite groups and some consequences, Proc. Nat. Acad. Sci. 48 6 (1962) 968-970 [jstor:71265]

Formalization in Coq:

Last revised on February 26, 2025 at 03:00:47. See the history of this page for a list of all contributions to it.